So the example would look like:
#x_4 == (-#y_2) * (2) && #y_2 == 3
right?

I'm just not super sure about this because it will have more disconnect from code right?
Lets say we have:
#x_4 == (-#z_3) * (2) && #z_3 == #y_2 && #y_2 == 3

That expression probably came from code like:

int y = 3;
int z = y;
@Refinement(...)
int x = -z *2;

If we are say that #x == (-#y) * (2) && #y_2 == 3 it can leave the user wondering why is x==y and we said it was x==z. It creates more disconnect between the error message and the code.

Now, if you are mentioning flattening variable instances for the same variable like y_1 and y_2, that makes more sense, since they are only internal representations but if we have a connection through a different variable, I'm not sure we should flatten it

You're right. Let me try only flattening variable instances for the same variable.

I think Catarina raises an interesting point, but with tens of variables, I'm not sure I would want to play "connect the dots" with all variables.

In some cases, I want it all collapsed (to see that I am accessing out of bounds), and in other cases I would want (as Catarina) the connection to the variables in the code first and front.

We might need to write some more real-world examples to decide the best default behavior, but in principle, I like that we are able to simplify as most as possible, but then expand to connect to the source code.

Yeah maybe with very large programs it becomes useful, but for debugging it will be a pain to understand where each predicate is created. I think most examples we have are rather small but we can try creating some bigger ones to test it on